Nuprl Lemma : exists_over_and_r
9,38
postcript
pdf
T
:Type,
A
:
,
B
:(
T
). (
x
:
T
. (
A
B
(
x
)))
(
A
(
x
:
T
.
B
(
x
)))
latex
ProofTree
Definitions
t
T
,
P
Q
,
P
Q
,
x
(
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
origin
T:Type, A:
, B:(T
). (
x:T. (A 
B(x))) 
(A (x:T. B(x)))
T:Type, A:, B:(T). (x:T. (A B(x))) (A (x:T. B(x)))
T Q Q Qx:A. B(x) Qx:A. B(x)